/*
Copyright 2007 Laura Giordano, Valetina Gliozzi, Nicola Olivetti, Gian Luca Pozzato

    This file is part of FreeP.

    FreeP is free software: you can redistribute it and/or modify
    it under the terms of the GNU General Public License as published by
    the Free Software Foundation, either version 3 of the License, or
    (at your option) any later version.

    FreeP is distributed in the hope that it will be useful,
    but WITHOUT ANY WARRANTY; without even the implied warranty of
    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
    GNU General Public License for more details.

    You should have received a copy of the GNU General Public License
    along with FreeP.  If not, see <http://www.gnu.org/licenses/>.
*/

:- op(400,xfy,<), 
   op(400,fy,neg), 
   op(400,fy,box),
   op(500,xfy,and), 
   op(600,xfy,or),
   op(650,xfy,->), 
   op(650,xfy,=>).
   
:-use_module(library(random)).
:-use_module(library(lists)).
:-use_module(library(timeout)).
:-use_module(library(clpfd)).

:-dynamic flat/0.


/* ---------------------------------------------------------------- */
/* To prove if Gamma is unsatisfiable, call
   
	prove(Gamma,[],1,[],[],_,[],Tree)

    The above predicate if and only if Gamma is unsatisfiable.
    In this case, Tree contains a closed tableau for Gamma
*/
/* ---------------------------------------------------------------- */


/* ------------------------------------------------------------------------------------------------------------- */
/* Axioms: try to close the current branch of the tableau */
/* ------------------------------------------------------------------------------------------------------------- */

prove(Gamma,_,_,Used,WildCards,[],_,tree(axiom)):-
  member([X,A],Gamma),
  member([Y,neg A],Gamma),
  matchList(X,Y),
  constr(Used),
  constrWildCards(WildCards),!,
  asserta(flat). 
prove(Gamma,Sigma,_,Used,WildCards,[Fml],_,tree(axiom)):-
		    member([[V|X],A],Sigma),
		    member([Y,neg A],Gamma),
		    copyFormula([[V|X],A],Fml),
		    split(Y,PrefY,SuffY),
		    V=PrefY,
		    matchList(SuffY,X),
		    constr(Used),
                    constrWildCards(WildCards),!,
		    asserta(flat). 
prove(Gamma,Sigma,_,Used,WildCards,[Fml],_,tree(axiom)):-
		    member([[V|X],neg A],Sigma),
		    member([Y,A],Gamma),
		    copyFormula([[V|X],neg A],Fml),
		    split(Y,PrefY,SuffY),
		    V=PrefY,
		    matchList(SuffY,X),
		    constr(Used),
                    constrWildCards(WildCards),!,
  		    asserta(flat). 
		      
/* ------------------------------------------------------------------------------------------------------------- */		      
/* If a branch has been closed, we may need to flat the labels obtained after the pattern matching */  
/* ------------------------------------------------------------------------------------------------------------- */
		    
proveAux(Gamma,Sigma,Max,Used,WildCards,AddedSigma,RecoverSigma,Tree):-
  (flat,flatten(Gamma,NewGamma),flatten(Sigma,NewSigma),retractall(flat),
   remove_duplicates(NewGamma,DefGamma),remove_duplicates(NewSigma,DefSigma),
   prove(DefGamma,DefSigma,Max,Used,WildCards,AddedSigma,RecoverSigma,Tree));
  remove_duplicates(Gamma,PrunedGamma),remove_duplicates(Sigma,PrunedSigma),
  prove(PrunedGamma,PrunedSigma,Max,Used,WildCards,AddedSigma,RecoverSigma,Tree).
  

/* ------------------------------------------------------------------------------------------------------------- */		      
/* Makes a copy of a formula containing free variables in its label */
/* ------------------------------------------------------------------------------------------------------------- */		      
copyFormula([Label,Fml],[CopiedLabel,Fml]):-auxCopy(Label,CopiedLabel),!.
auxCopy([],[]):-!.
auxCopy([Variable|Tail],[_|ResTail]):-var(Variable),auxCopy(Tail,ResTail).
auxCopy([Constant|Tail],[Constant|ResTail]):-nonvar(Constant),auxCopy(Tail,ResTail).
  
  
/* ------------------------------------------------------------------------------------------------------------- */		      
/* Rules of the calculi */  
/* ------------------------------------------------------------------------------------------------------------- */

/* ------------------------------------------------------------------------------------------------------------- */
/* Boolean connectives with one conclusion in Gamma */

prove(Gamma,Sigma,Max,Used,WildCards,AddedSigma,RecoverSigma,tree(neg,[Label,neg neg F],SubTree)):-
  select([Label,neg neg F],Gamma,NewGamma),!,
  prove([[Label,F]|NewGamma],Sigma,Max,Used,WildCards,AddedSigma,RecoverSigma,SubTree).
  
prove(Gamma,Sigma,Max,Used,WildCards,AddedSigma,RecoverSigma,tree(impN,[Label,neg(F->G)],SubTree)):-
  select([Label,neg(F->G)],Gamma,NewGamma),!,
  prove([[Label,F]|[[Label,neg G]|NewGamma]],Sigma,Max,Used,WildCards,AddedSigma,RecoverSigma,SubTree).
  
prove(Gamma,Sigma,Max,Used,WildCards,AddedSigma,RecoverSigma,tree(andP,[Label,F and G],SubTree)):-
  select([Label,F and G],Gamma,NewGamma),!,
  prove([[Label,F]|[[Label,G]|NewGamma]],Sigma,Max,Used,WildCards,AddedSigma,RecoverSigma,SubTree).

prove(Gamma,Sigma,Max,Used,WildCards,AddedSigma,RecoverSigma,tree(orN,[Label,neg (F or G)],SubTree)):-
  select([Label,neg (F or G)],Gamma,NewGamma),!,
  prove([[Label,neg F]|[[Label,neg G]|NewGamma]],Sigma,Max,Used,WildCards,AddedSigma,RecoverSigma,SubTree).



/* ------------------------------------------------------------------------------------------------------------- */
/* Boolean connectives introducing a branch in Gamma */

prove(Gamma,Sigma,Max,Used,WildCards,AddedSigma,RecoverSigma,tree(impP,[Label,F->G],LeftTree,RightTree)):-
  select([Label,F->G],Gamma,NewGamma),!,
  prove([[Label,neg F]|NewGamma],Sigma,Max,Used,WildCards,LeftAdded,RecoverSigma,LeftTree),!,
  append(LeftAdded,Sigma,DefSigma),
  proveAux([[Label,G]|NewGamma],DefSigma,Max,Used,WildCards,RightAdded,RecoverSigma,RightTree),
  append(LeftAdded,RightAdded,AddedSigma).
  
prove(Gamma,Sigma,Max,Used,WildCards,AddedSigma,RecoverSigma,tree(andN,[Label,neg (F and G)],LeftTree,RightTree)):-
  select([Label,neg (F and G)],Gamma,NewGamma),!,
  prove([[Label,neg F]|NewGamma],Sigma,Max,Used,WildCards,LeftAdded,RecoverSigma,LeftTree),!,
  append(LeftAdded,Sigma,DefSigma),
  proveAux([[Label,neg G]|NewGamma],DefSigma,Max,Used,WildCards,RightAdded,RecoverSigma,RightTree),
  append(LeftAdded,RightAdded,AddedSigma).

prove(Gamma,Sigma,Max,Used,WildCards,AddedSigma,RecoverSigma,tree(orP,[Label,F or G],LeftTree,RightTree)):-
  select([Label,F or G],Gamma,NewGamma),!,
  prove([[Label,F]|NewGamma],Sigma,Max,Used,WildCards,LeftAdded,RecoverSigma,LeftTree),!,
  append(LeftAdded,Sigma,DefSigma),
  proveAux([[Label,G]|NewGamma],DefSigma,Max,Used,WildCards,RightAdded,RecoverSigma,RightTree),
  append(LeftAdded,RightAdded,AddedSigma).
  

/* ------------------------------------------------------------------------------------------------------------- */
/* Recover of formulas from Sigma */
/* ------------------------------------------------------------------------------------------------------------- */

prove(Gamma,Sigma,Max,Used,WildCards,[Fml|AddedSigma],RecoverSigma,tree(inst,[[V|X],F],SubTree)):-
		    member([[V|X],F],Sigma),
		    member([Y,_],Gamma),
		    copyFormula([[V|X],F],Fml),
		    split(Y,PrefY,SuffY),
		    noVars(PrefY),
		    atLeastOneConstant(SuffY), 
		    V=PrefY,
		    matchList(SuffY,X),
		    flat([V|X],FlatVX),
		    \+member([FlatVX,F],RecoverSigma),!,
		    asserta(flat),
		    proveAux([[FlatVX,F]|Gamma],[Fml|Sigma],Max,Used,WildCards,AddedSigma,[[FlatVX,F]|RecoverSigma],SubTree).	    
  
/* ------------------------------------------------------------------------------------------------------------- */
/* Conditional connetives in Gamma (in Sigma these formulas cannot occurr) */  

prove(Gamma,Sigma,Max,Used,WildCards,CleanAdded,RecoverSigma,tree(entN,[U,neg(A=>B)],SubTree)):-
  select([U,neg(A=>B)],Gamma,NewGamma),!,
  N#=Max+1,
  proveAux([[[N],neg B]|[[[N],A]|NewGamma]],[[[_|[N]],neg A]|Sigma],N,Used,WildCards,AddedSigma,RecoverSigma,SubTree),
  cleanAdded(AddedSigma,[[_|[N]],neg A],CleanAdded).
  
prove(Gamma,Sigma,Max,Used,WildCards,AddedSigma,RecoverSigma,tree(entP,[U,A=>B],LeftTree,RightTree)):-
  member([U,A=>B],Gamma),
  \+member([A=>B,_,_],Used),!,
  prove([[[X],A->B]|Gamma],Sigma,Max,[[A=>B,1,[[X]]]|Used],[[X,Max]|WildCards],LeftAdded,RecoverSigma,LeftTree),!,
  N#=Max+1, 
  append(LeftAdded,Sigma,DefSigma),
  proveAux([[[N|[X]],A]|Gamma],[[[_|[N|[X]]],neg A]|DefSigma],N,[[A=>B,1,[[X]]]|Used],
      [[X,Max]|WildCards],RightAdded,RecoverSigma,RightTree),!,
  cleanAdded(RightAdded,[[_|[N|[X]]],neg A],RightCleanAdded),
  append(LeftAdded,RightCleanAdded,AddedSigma).

prove(Gamma,Sigma,Max,Used,WildCards,AddedSigma,RecoverSigma,tree(entP,[U,A=>B],LeftTree,RightTree)):-
  memberBest(A=>B,Used),
  member([U,A=>B],Gamma),
  select([A=>B,NumOfWildCards,PreviousWildCards],Used,NewUsed),
  NumOfWildCards<Max,!,
  NewWildCards#=NumOfWildCards+1,
  prove([[[X],A->B]|Gamma],Sigma,Max,[[A=>B,NewWildCards,[[X]|PreviousWildCards]]|NewUsed],
      [[X,Max]|WildCards],LeftAdded,RecoverSigma,LeftTree),!,
  N#=Max+1, 
  append(LeftAdded,Sigma,DefSigma),
  proveAux([[[N|[X]],A]|Gamma],[[[_|[N|[X]]],neg A]|DefSigma],N,
      [[A=>B,NewWildCards,[[X]|PreviousWildCards]]|NewUsed],[[X,Max]|WildCards],RightAdded,RecoverSigma,RightTree),!,
  cleanAdded(RightAdded,[[_|[N|[X]]],neg A],RightCleanAdded),
  append(LeftAdded,RightCleanAdded,AddedSigma).

/* ------------------------------------------------------------------------------------------------------------- */
   /* This predicate succeeds if and only if the two arguments match. A free variable in each list
   represent any list */
matchList([],[]).
matchList([Variable],List):-var(Variable),no_doubles([Variable|List]),List=Variable.
matchList(List,[Variable]):-var(Variable),no_doubles([Variable|List]),List=Variable.
matchList([Constant|Tail1],[Constant|Tail2]):-nonvar(Constant),matchList(Tail1,Tail2).
matchList([Constant|Tail1],[Variable|Tail2]):-
     nonvar(Constant),var(Variable),split([Constant|Tail1],Prefix,Suffix),matchList(Suffix,Tail2),Prefix=Variable.
matchList([Variable|Tail1],List):-var(Variable),split(List,Prefix,Suffix),matchList(Tail1,Suffix),Prefix=Variable.


/* ------------------------------------------------------------------------------------------------------------- */
   /* This predicate finds a formula A=>B in Gamma such that the number of applications of (|~+) 
      in the current branch is minimal */
memberBest(A=>B,Used):-buildListOfNumOfWildCards(Used,LNWC),min_list(LNWC,Min),member([A=>B,Min,_],Used).

buildListOfNumOfWildCards([],[]):-!.
buildListOfNumOfWildCards([[_,Number,_]|Tail],[Number|ResTail]):-buildListOfNumOfWildCards(Tail,ResTail).
 

/* ------------------------------------------------------------------------------------------------------------- */
/* Removes from the list the first item matching with the second argument */
cleanAdded(List,[Label|Formula],Result):-
  flatten(List,FlattenedList), /* Regionarci su: forse non è necessaria */
  flat(Label,FlattenedLabel), /* Necessaria */
  cleanAddedAux(FlattenedList,[FlattenedLabel|Formula],Result).
cleanAddedAux([],_,[]):-!.  
cleanAddedAux([[Label1,Fml]|Tail],[Label2,Fml],Tail):-
  strictMatchList(Label1,Label2),!.
cleanAddedAux([Head|Tail],LabelledFormula,[Head|CleanedTail]):-
  cleanAddedAux(Tail,LabelledFormula,CleanedTail).


/* ------------------------------------------------------------------------------------------------------------- */
/* This predicate verifies if two labels match in a strict way, namely 
   if all their corresponding elements match */
strictMatchList([],[]):-!.
strictMatchList([V1|Tail1],[V2|Tail2]):-
  var(V1),var(V2),strictMatchList(Tail1,Tail2).
strictMatchList([Constant|Tail1],[Constant|Tail2]):-
  nonvar(Constant),strictMatchList(Tail1,Tail2).
  
  
/* ------------------------------------------------------------------------------------------------------------- */
/* Invoked when a branch is closed, it checks if all variables introduced to apply (|~+) on the same
   formula A|~B are all different */
/* ------------------------------------------------------------------------------------------------------------- */
constr([]):-!.
constr([[_,_,WildCards]|Tail]):-flatLabels(WildCards,FlattedCards),no_doubles(FlattedCards),constr(Tail).


/* ------------------------------------------------------------------------------------------------------------- */
/* Invoked when a branch is closed, it checks if all wildcards free-variables introduced to apply (|~+) 
   have been instantiated with an available label, i.e. with a label occurring in the node when the
   wildcard free-variable is introduced */
/* ------------------------------------------------------------------------------------------------------------- */
constrWildCards([]):-!.
constrWildCards([[WildCard,Max]|Tail]):-
  flat(WildCard,FlattedCard),
  allAvailable(FlattedCard,Max),
  constrWildCards(Tail).

allAvailable([],_):-!.
allAvailable([[]|_],_):-!,fail.
allAvailable([Head|Tail],Max):-var(Head),allAvailable(Tail,Max).
allAvailable([Head|Tail],Max):-nonvar(Head),Head=<Max,allAvailable(Tail,Max).

/* ------------------------------------------------------------------------------------------------------------- */
/* Given a list of formulas or labels, it flattens all the labels */
/* ------------------------------------------------------------------------------------------------------------- */
flatten([],[]):-!.
flatten([[Variable,Formula]|Tail],[[Variable,Formula]|FlattenedTail]):-
  var(Variable),!,
  flatten(Tail,FlattenedTail).
flatten([[Label,Formula]|Tail],[[FlattenedLabel,Formula]|FlattenedTail]):-
  flat(Label,FlattenedLabel),
  flatten(Tail,FlattenedTail).
  
flatLabels([],[]):-!.
flatLabels([Variable|Tail],[Variable|FlattenedTail]):-
  var(Variable),!,
  flatLabels(Tail,FlattenedTail).
flatLabels([Label|Tail],[FlattenedLabel|FlattenedTail]):-
  flat(Label,FlattenedLabel),
  flatLabels(Tail,FlattenedTail).

flat([],[]):-!.
flat([Variable|Tail],[Variable|FlattenedTail]):-
  var(Variable),!,
  flat(Tail,FlattenedTail).
flat([Atom|Tail],[Atom|FlattenedTail]):-
  atomic(Atom),!,
  flat(Tail,FlattenedTail).
flat([Head|Tail],FlattenedList):-
  flat(Head,FlattenedHead),
  flat(Tail,FlattenedTail),
  append(FlattenedHead,FlattenedTail,FlattenedList).
  
  
    
/* ------------------------------------------------------------------------------------------------------------- */
/* Auxiliary predicates managing free variables labels */
/* ------------------------------------------------------------------------------------------------------------- */

atLeastOneConstant([Head|_]):-nonvar(Head),!.
atLeastOneConstant([_|Tail]):-atLeastOneConstant(Tail).

split(List,Prefix,Suffix):-auxSplit(List,Prefix,Suffix,1).
auxSplit(List,Prefix,Suffix,Pos):-
    firstNElements(List,Prefix,Pos),
    lastNElements(List,Suffix,Pos).
auxSplit(List,Prefix,Suffix,Pos):-Pos1 is Pos+1,length(List,L),Pos1<L,auxSplit(List,Prefix,Suffix,Pos1).
    


/* Returns a list with the first N elements of the first argument L, with N<=length(L) */		    
firstNElements(_,[],0):-!.
firstNElements([Head|Tail],[Head|ResTail],Pos):-Pos1 is Pos-1,firstNElements(Tail,ResTail,Pos1).

/* Returns the sublist starting from the element in position N */
lastNElements(List,List,0):-!.
lastNElements([_|Tail],Res,Pos):-Pos1 is Pos-1,lastNElements(Tail,Res,Pos1).

/* noVars succeeds if and only if the argument is a list not containing variables */
noVars([]):-!.
noVars([Head|Tail]):-nonvar(Head),noVars(Tail).